(0) Obligation:
Clauses:
add(b, b, b).
add(X, b, X) :- binaryZ(X).
add(b, Y, Y) :- binaryZ(Y).
add(X, Y, Z) :- addz(X, Y, Z).
addx(one(X), b, one(X)) :- binary(X).
addx(zero(X), b, zero(X)) :- binaryZ(X).
addx(X, Y, Z) :- addz(X, Y, Z).
addy(b, one(Y), one(Y)) :- binary(Y).
addy(b, zero(Y), zero(Y)) :- binaryZ(Y).
addy(X, Y, Z) :- addz(X, Y, Z).
addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z).
addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z).
addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z).
addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z).
addc(b, b, one(b)).
addc(X, b, Z) :- succZ(X, Z).
addc(b, Y, Z) :- succZ(Y, Z).
addc(X, Y, Z) :- addC(X, Y, Z).
addX(zero(X), b, one(X)) :- binaryZ(X).
addX(one(X), b, zero(Z)) :- succ(X, Z).
addX(X, Y, Z) :- addC(X, Y, Z).
addY(b, zero(Y), one(Y)) :- binaryZ(Y).
addY(b, one(Y), zero(Z)) :- succ(Y, Z).
addY(X, Y, Z) :- addC(X, Y, Z).
addC(zero(X), zero(Y), one(Z)) :- addz(X, Y, Z).
addC(zero(X), one(Y), zero(Z)) :- addX(X, Y, Z).
addC(one(X), zero(Y), zero(Z)) :- addY(X, Y, Z).
addC(one(X), one(Y), one(Z)) :- addc(X, Y, Z).
binary(b).
binary(zero(X)) :- binaryZ(X).
binary(one(X)) :- binary(X).
binaryZ(zero(X)) :- binaryZ(X).
binaryZ(one(X)) :- binary(X).
succ(b, one(b)).
succ(zero(X), one(X)) :- binaryZ(X).
succ(one(X), zero(Z)) :- succ(X, Z).
succZ(zero(X), one(X)) :- binaryZ(X).
succZ(one(X), zero(Z)) :- succ(X, Z).
times(one(b), X, X).
times(zero(R), S, zero(RS)) :- times(R, S, RS).
times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS)).
Query: add(a,a,g)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
binaryZA(zero(X1)) :- binaryZA(X1).
binaryZA(one(X1)) :- binaryB(X1).
binaryB(zero(X1)) :- binaryZA(X1).
binaryB(one(X1)) :- binaryB(X1).
addzC(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addzC(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addzC(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addzC(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
succG(zero(X1), one(X1)) :- binaryZA(X1).
succG(one(X1), zero(X2)) :- succG(X1, X2).
succZH(zero(X1), one(X1)) :- binaryZA(X1).
succZH(one(X1), zero(X2)) :- succG(X1, X2).
addCI(zero(X1), zero(X2), one(X3)) :- addzC(X1, X2, X3).
addCI(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZA(X1).
addCI(zero(one(X1)), one(b), zero(zero(X2))) :- succG(X1, X2).
addCI(zero(X1), one(X2), zero(X3)) :- addCI(X1, X2, X3).
addCI(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZA(X1).
addCI(one(b), zero(one(X1)), zero(zero(X2))) :- succG(X1, X2).
addCI(one(X1), zero(X2), zero(X3)) :- addCI(X1, X2, X3).
addCI(one(X1), one(X2), one(X3)) :- addcF(X1, X2, X3).
addcF(X1, b, X2) :- succZH(X1, X2).
addcF(b, X1, X2) :- succZH(X1, X2).
addcF(X1, X2, X3) :- addCI(X1, X2, X3).
addxD(one(X1), b, one(X1)) :- binaryB(X1).
addxD(zero(X1), b, zero(X1)) :- binaryZA(X1).
addxD(X1, X2, X3) :- addzC(X1, X2, X3).
addyE(b, one(X1), one(X1)) :- binaryB(X1).
addyE(b, zero(X1), zero(X1)) :- binaryZA(X1).
addyE(X1, X2, X3) :- addzC(X1, X2, X3).
addzJ(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addzJ(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addzJ(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addzJ(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
addK(X1, X2, b) :- addzL(X1, X2).
addK(X1, X2, b) :- addzL(X1, X2).
addK(zero(X1), b, zero(X1)) :- binaryZA(X1).
addK(one(X1), b, one(X1)) :- binaryB(X1).
addK(b, X1, X1) :- binaryZA(X1).
addK(X1, X2, X3) :- addzJ(X1, X2, X3).
addK(b, zero(X1), zero(X1)) :- binaryZA(X1).
addK(b, one(X1), one(X1)) :- binaryB(X1).
addK(X1, X2, X3) :- addzJ(X1, X2, X3).
addK(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addK(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addK(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addK(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
Clauses:
binaryZcA(zero(X1)) :- binaryZcA(X1).
binaryZcA(one(X1)) :- binarycB(X1).
binarycB(b).
binarycB(zero(X1)) :- binaryZcA(X1).
binarycB(one(X1)) :- binarycB(X1).
addzcC(zero(X1), zero(X2), zero(X3)) :- addzcC(X1, X2, X3).
addzcC(zero(X1), one(X2), one(X3)) :- addxcD(X1, X2, X3).
addzcC(one(X1), zero(X2), one(X3)) :- addycE(X1, X2, X3).
addzcC(one(X1), one(X2), zero(X3)) :- addccF(X1, X2, X3).
succcG(b, one(b)).
succcG(zero(X1), one(X1)) :- binaryZcA(X1).
succcG(one(X1), zero(X2)) :- succcG(X1, X2).
succZcH(zero(X1), one(X1)) :- binaryZcA(X1).
succZcH(one(X1), zero(X2)) :- succcG(X1, X2).
addCcI(zero(X1), zero(X2), one(X3)) :- addzcC(X1, X2, X3).
addCcI(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZcA(X1).
addCcI(zero(one(X1)), one(b), zero(zero(X2))) :- succcG(X1, X2).
addCcI(zero(X1), one(X2), zero(X3)) :- addCcI(X1, X2, X3).
addCcI(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZcA(X1).
addCcI(one(b), zero(one(X1)), zero(zero(X2))) :- succcG(X1, X2).
addCcI(one(X1), zero(X2), zero(X3)) :- addCcI(X1, X2, X3).
addCcI(one(X1), one(X2), one(X3)) :- addccF(X1, X2, X3).
addccF(b, b, one(b)).
addccF(X1, b, X2) :- succZcH(X1, X2).
addccF(b, X1, X2) :- succZcH(X1, X2).
addccF(X1, X2, X3) :- addCcI(X1, X2, X3).
addxcD(one(X1), b, one(X1)) :- binarycB(X1).
addxcD(zero(X1), b, zero(X1)) :- binaryZcA(X1).
addxcD(X1, X2, X3) :- addzcC(X1, X2, X3).
addycE(b, one(X1), one(X1)) :- binarycB(X1).
addycE(b, zero(X1), zero(X1)) :- binaryZcA(X1).
addycE(X1, X2, X3) :- addzcC(X1, X2, X3).
addzcJ(zero(X1), zero(X2), zero(X3)) :- addzcC(X1, X2, X3).
addzcJ(zero(X1), one(X2), one(X3)) :- addxcD(X1, X2, X3).
addzcJ(one(X1), zero(X2), one(X3)) :- addycE(X1, X2, X3).
addzcJ(one(X1), one(X2), zero(X3)) :- addccF(X1, X2, X3).
Afs:
addK(x1, x2, x3) = addK(x3)
(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)
Deleted triples and predicates having undefined goals [DT09].
(4) Obligation:
Triples:
binaryZA(zero(X1)) :- binaryZA(X1).
binaryZA(one(X1)) :- binaryB(X1).
binaryB(zero(X1)) :- binaryZA(X1).
binaryB(one(X1)) :- binaryB(X1).
addzC(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addzC(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addzC(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addzC(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
succG(zero(X1), one(X1)) :- binaryZA(X1).
succG(one(X1), zero(X2)) :- succG(X1, X2).
succZH(zero(X1), one(X1)) :- binaryZA(X1).
succZH(one(X1), zero(X2)) :- succG(X1, X2).
addCI(zero(X1), zero(X2), one(X3)) :- addzC(X1, X2, X3).
addCI(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZA(X1).
addCI(zero(one(X1)), one(b), zero(zero(X2))) :- succG(X1, X2).
addCI(zero(X1), one(X2), zero(X3)) :- addCI(X1, X2, X3).
addCI(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZA(X1).
addCI(one(b), zero(one(X1)), zero(zero(X2))) :- succG(X1, X2).
addCI(one(X1), zero(X2), zero(X3)) :- addCI(X1, X2, X3).
addCI(one(X1), one(X2), one(X3)) :- addcF(X1, X2, X3).
addcF(X1, b, X2) :- succZH(X1, X2).
addcF(b, X1, X2) :- succZH(X1, X2).
addcF(X1, X2, X3) :- addCI(X1, X2, X3).
addxD(one(X1), b, one(X1)) :- binaryB(X1).
addxD(zero(X1), b, zero(X1)) :- binaryZA(X1).
addxD(X1, X2, X3) :- addzC(X1, X2, X3).
addyE(b, one(X1), one(X1)) :- binaryB(X1).
addyE(b, zero(X1), zero(X1)) :- binaryZA(X1).
addyE(X1, X2, X3) :- addzC(X1, X2, X3).
addzJ(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addzJ(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addzJ(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addzJ(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
addK(zero(X1), b, zero(X1)) :- binaryZA(X1).
addK(one(X1), b, one(X1)) :- binaryB(X1).
addK(b, X1, X1) :- binaryZA(X1).
addK(X1, X2, X3) :- addzJ(X1, X2, X3).
addK(b, zero(X1), zero(X1)) :- binaryZA(X1).
addK(b, one(X1), one(X1)) :- binaryB(X1).
addK(X1, X2, X3) :- addzJ(X1, X2, X3).
addK(zero(X1), zero(X2), zero(X3)) :- addzC(X1, X2, X3).
addK(zero(X1), one(X2), one(X3)) :- addxD(X1, X2, X3).
addK(one(X1), zero(X2), one(X3)) :- addyE(X1, X2, X3).
addK(one(X1), one(X2), zero(X3)) :- addcF(X1, X2, X3).
Clauses:
binaryZcA(zero(X1)) :- binaryZcA(X1).
binaryZcA(one(X1)) :- binarycB(X1).
binarycB(b).
binarycB(zero(X1)) :- binaryZcA(X1).
binarycB(one(X1)) :- binarycB(X1).
addzcC(zero(X1), zero(X2), zero(X3)) :- addzcC(X1, X2, X3).
addzcC(zero(X1), one(X2), one(X3)) :- addxcD(X1, X2, X3).
addzcC(one(X1), zero(X2), one(X3)) :- addycE(X1, X2, X3).
addzcC(one(X1), one(X2), zero(X3)) :- addccF(X1, X2, X3).
succcG(b, one(b)).
succcG(zero(X1), one(X1)) :- binaryZcA(X1).
succcG(one(X1), zero(X2)) :- succcG(X1, X2).
succZcH(zero(X1), one(X1)) :- binaryZcA(X1).
succZcH(one(X1), zero(X2)) :- succcG(X1, X2).
addCcI(zero(X1), zero(X2), one(X3)) :- addzcC(X1, X2, X3).
addCcI(zero(zero(X1)), one(b), zero(one(X1))) :- binaryZcA(X1).
addCcI(zero(one(X1)), one(b), zero(zero(X2))) :- succcG(X1, X2).
addCcI(zero(X1), one(X2), zero(X3)) :- addCcI(X1, X2, X3).
addCcI(one(b), zero(zero(X1)), zero(one(X1))) :- binaryZcA(X1).
addCcI(one(b), zero(one(X1)), zero(zero(X2))) :- succcG(X1, X2).
addCcI(one(X1), zero(X2), zero(X3)) :- addCcI(X1, X2, X3).
addCcI(one(X1), one(X2), one(X3)) :- addccF(X1, X2, X3).
addccF(b, b, one(b)).
addccF(X1, b, X2) :- succZcH(X1, X2).
addccF(b, X1, X2) :- succZcH(X1, X2).
addccF(X1, X2, X3) :- addCcI(X1, X2, X3).
addxcD(one(X1), b, one(X1)) :- binarycB(X1).
addxcD(zero(X1), b, zero(X1)) :- binaryZcA(X1).
addxcD(X1, X2, X3) :- addzcC(X1, X2, X3).
addycE(b, one(X1), one(X1)) :- binarycB(X1).
addycE(b, zero(X1), zero(X1)) :- binaryZcA(X1).
addycE(X1, X2, X3) :- addzcC(X1, X2, X3).
addzcJ(zero(X1), zero(X2), zero(X3)) :- addzcC(X1, X2, X3).
addzcJ(zero(X1), one(X2), one(X3)) :- addxcD(X1, X2, X3).
addzcJ(one(X1), zero(X2), one(X3)) :- addycE(X1, X2, X3).
addzcJ(one(X1), one(X2), zero(X3)) :- addccF(X1, X2, X3).
Afs:
addK(x1, x2, x3) = addK(x3)
(5) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
addK_in: (f,f,b)
binaryZA_in: (b)
binaryB_in: (b)
addzJ_in: (f,f,b)
addzC_in: (f,f,b)
addxD_in: (f,f,b)
addyE_in: (f,f,b)
addcF_in: (f,f,b)
succZH_in: (f,b)
succG_in: (f,b)
addCI_in: (f,f,b)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
ADDK_IN_AAG(zero(X1), b, zero(X1)) → U34_AAG(X1, binaryZA_in_g(X1))
ADDK_IN_AAG(zero(X1), b, zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(zero(X1)) → U1_G(X1, binaryZA_in_g(X1))
BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(one(X1)) → U2_G(X1, binaryB_in_g(X1))
BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
BINARYB_IN_G(zero(X1)) → U3_G(X1, binaryZA_in_g(X1))
BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYB_IN_G(one(X1)) → U4_G(X1, binaryB_in_g(X1))
BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
ADDK_IN_AAG(one(X1), b, one(X1)) → U35_AAG(X1, binaryB_in_g(X1))
ADDK_IN_AAG(one(X1), b, one(X1)) → BINARYB_IN_G(X1)
ADDK_IN_AAG(b, X1, X1) → U36_AAG(X1, binaryZA_in_g(X1))
ADDK_IN_AAG(b, X1, X1) → BINARYZA_IN_G(X1)
ADDK_IN_AAG(X1, X2, X3) → U37_AAG(X1, X2, X3, addzJ_in_aag(X1, X2, X3))
ADDK_IN_AAG(X1, X2, X3) → ADDZJ_IN_AAG(X1, X2, X3)
ADDZJ_IN_AAG(zero(X1), zero(X2), zero(X3)) → U30_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDZJ_IN_AAG(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(zero(X1), zero(X2), zero(X3)) → U5_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDZC_IN_AAG(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(zero(X1), one(X2), one(X3)) → U6_AAG(X1, X2, X3, addxD_in_aag(X1, X2, X3))
ADDZC_IN_AAG(zero(X1), one(X2), one(X3)) → ADDXD_IN_AAG(X1, X2, X3)
ADDXD_IN_AAG(one(X1), b, one(X1)) → U24_AAG(X1, binaryB_in_g(X1))
ADDXD_IN_AAG(one(X1), b, one(X1)) → BINARYB_IN_G(X1)
ADDXD_IN_AAG(zero(X1), b, zero(X1)) → U25_AAG(X1, binaryZA_in_g(X1))
ADDXD_IN_AAG(zero(X1), b, zero(X1)) → BINARYZA_IN_G(X1)
ADDXD_IN_AAG(X1, X2, X3) → U26_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDXD_IN_AAG(X1, X2, X3) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(one(X1), zero(X2), one(X3)) → U7_AAG(X1, X2, X3, addyE_in_aag(X1, X2, X3))
ADDZC_IN_AAG(one(X1), zero(X2), one(X3)) → ADDYE_IN_AAG(X1, X2, X3)
ADDYE_IN_AAG(b, one(X1), one(X1)) → U27_AAG(X1, binaryB_in_g(X1))
ADDYE_IN_AAG(b, one(X1), one(X1)) → BINARYB_IN_G(X1)
ADDYE_IN_AAG(b, zero(X1), zero(X1)) → U28_AAG(X1, binaryZA_in_g(X1))
ADDYE_IN_AAG(b, zero(X1), zero(X1)) → BINARYZA_IN_G(X1)
ADDYE_IN_AAG(X1, X2, X3) → U29_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDYE_IN_AAG(X1, X2, X3) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(one(X1), one(X2), zero(X3)) → U8_AAG(X1, X2, X3, addcF_in_aag(X1, X2, X3))
ADDZC_IN_AAG(one(X1), one(X2), zero(X3)) → ADDCF_IN_AAG(X1, X2, X3)
ADDCF_IN_AAG(X1, b, X2) → U21_AAG(X1, X2, succZH_in_ag(X1, X2))
ADDCF_IN_AAG(X1, b, X2) → SUCCZH_IN_AG(X1, X2)
SUCCZH_IN_AG(zero(X1), one(X1)) → U11_AG(X1, binaryZA_in_g(X1))
SUCCZH_IN_AG(zero(X1), one(X1)) → BINARYZA_IN_G(X1)
SUCCZH_IN_AG(one(X1), zero(X2)) → U12_AG(X1, X2, succG_in_ag(X1, X2))
SUCCZH_IN_AG(one(X1), zero(X2)) → SUCCG_IN_AG(X1, X2)
SUCCG_IN_AG(zero(X1), one(X1)) → U9_AG(X1, binaryZA_in_g(X1))
SUCCG_IN_AG(zero(X1), one(X1)) → BINARYZA_IN_G(X1)
SUCCG_IN_AG(one(X1), zero(X2)) → U10_AG(X1, X2, succG_in_ag(X1, X2))
SUCCG_IN_AG(one(X1), zero(X2)) → SUCCG_IN_AG(X1, X2)
ADDCF_IN_AAG(b, X1, X2) → U22_AAG(X1, X2, succZH_in_ag(X1, X2))
ADDCF_IN_AAG(b, X1, X2) → SUCCZH_IN_AG(X1, X2)
ADDCF_IN_AAG(X1, X2, X3) → U23_AAG(X1, X2, X3, addCI_in_aag(X1, X2, X3))
ADDCF_IN_AAG(X1, X2, X3) → ADDCI_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(zero(X1), zero(X2), one(X3)) → U13_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDCI_IN_AAG(zero(X1), zero(X2), one(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(zero(zero(X1)), one(b), zero(one(X1))) → U14_AAG(X1, binaryZA_in_g(X1))
ADDCI_IN_AAG(zero(zero(X1)), one(b), zero(one(X1))) → BINARYZA_IN_G(X1)
ADDCI_IN_AAG(zero(one(X1)), one(b), zero(zero(X2))) → U15_AAG(X1, X2, succG_in_ag(X1, X2))
ADDCI_IN_AAG(zero(one(X1)), one(b), zero(zero(X2))) → SUCCG_IN_AG(X1, X2)
ADDCI_IN_AAG(zero(X1), one(X2), zero(X3)) → U16_AAG(X1, X2, X3, addCI_in_aag(X1, X2, X3))
ADDCI_IN_AAG(zero(X1), one(X2), zero(X3)) → ADDCI_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(one(b), zero(zero(X1)), zero(one(X1))) → U17_AAG(X1, binaryZA_in_g(X1))
ADDCI_IN_AAG(one(b), zero(zero(X1)), zero(one(X1))) → BINARYZA_IN_G(X1)
ADDCI_IN_AAG(one(b), zero(one(X1)), zero(zero(X2))) → U18_AAG(X1, X2, succG_in_ag(X1, X2))
ADDCI_IN_AAG(one(b), zero(one(X1)), zero(zero(X2))) → SUCCG_IN_AG(X1, X2)
ADDCI_IN_AAG(one(X1), zero(X2), zero(X3)) → U19_AAG(X1, X2, X3, addCI_in_aag(X1, X2, X3))
ADDCI_IN_AAG(one(X1), zero(X2), zero(X3)) → ADDCI_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(one(X1), one(X2), one(X3)) → U20_AAG(X1, X2, X3, addcF_in_aag(X1, X2, X3))
ADDCI_IN_AAG(one(X1), one(X2), one(X3)) → ADDCF_IN_AAG(X1, X2, X3)
ADDZJ_IN_AAG(zero(X1), one(X2), one(X3)) → U31_AAG(X1, X2, X3, addxD_in_aag(X1, X2, X3))
ADDZJ_IN_AAG(zero(X1), one(X2), one(X3)) → ADDXD_IN_AAG(X1, X2, X3)
ADDZJ_IN_AAG(one(X1), zero(X2), one(X3)) → U32_AAG(X1, X2, X3, addyE_in_aag(X1, X2, X3))
ADDZJ_IN_AAG(one(X1), zero(X2), one(X3)) → ADDYE_IN_AAG(X1, X2, X3)
ADDZJ_IN_AAG(one(X1), one(X2), zero(X3)) → U33_AAG(X1, X2, X3, addcF_in_aag(X1, X2, X3))
ADDZJ_IN_AAG(one(X1), one(X2), zero(X3)) → ADDCF_IN_AAG(X1, X2, X3)
ADDK_IN_AAG(b, zero(X1), zero(X1)) → U38_AAG(X1, binaryZA_in_g(X1))
ADDK_IN_AAG(b, zero(X1), zero(X1)) → BINARYZA_IN_G(X1)
ADDK_IN_AAG(b, one(X1), one(X1)) → U39_AAG(X1, binaryB_in_g(X1))
ADDK_IN_AAG(b, one(X1), one(X1)) → BINARYB_IN_G(X1)
ADDK_IN_AAG(zero(X1), zero(X2), zero(X3)) → U40_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDK_IN_AAG(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDK_IN_AAG(zero(X1), one(X2), one(X3)) → U41_AAG(X1, X2, X3, addxD_in_aag(X1, X2, X3))
ADDK_IN_AAG(zero(X1), one(X2), one(X3)) → ADDXD_IN_AAG(X1, X2, X3)
ADDK_IN_AAG(one(X1), zero(X2), one(X3)) → U42_AAG(X1, X2, X3, addyE_in_aag(X1, X2, X3))
ADDK_IN_AAG(one(X1), zero(X2), one(X3)) → ADDYE_IN_AAG(X1, X2, X3)
ADDK_IN_AAG(one(X1), one(X2), zero(X3)) → U43_AAG(X1, X2, X3, addcF_in_aag(X1, X2, X3))
ADDK_IN_AAG(one(X1), one(X2), zero(X3)) → ADDCF_IN_AAG(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
zero(
x1) =
zero(
x1)
binaryZA_in_g(
x1) =
binaryZA_in_g(
x1)
one(
x1) =
one(
x1)
binaryB_in_g(
x1) =
binaryB_in_g(
x1)
addzJ_in_aag(
x1,
x2,
x3) =
addzJ_in_aag(
x3)
addzC_in_aag(
x1,
x2,
x3) =
addzC_in_aag(
x3)
addxD_in_aag(
x1,
x2,
x3) =
addxD_in_aag(
x3)
addyE_in_aag(
x1,
x2,
x3) =
addyE_in_aag(
x3)
addcF_in_aag(
x1,
x2,
x3) =
addcF_in_aag(
x3)
succZH_in_ag(
x1,
x2) =
succZH_in_ag(
x2)
succG_in_ag(
x1,
x2) =
succG_in_ag(
x2)
addCI_in_aag(
x1,
x2,
x3) =
addCI_in_aag(
x3)
b =
b
ADDK_IN_AAG(
x1,
x2,
x3) =
ADDK_IN_AAG(
x3)
U34_AAG(
x1,
x2) =
U34_AAG(
x1,
x2)
BINARYZA_IN_G(
x1) =
BINARYZA_IN_G(
x1)
U1_G(
x1,
x2) =
U1_G(
x1,
x2)
U2_G(
x1,
x2) =
U2_G(
x1,
x2)
BINARYB_IN_G(
x1) =
BINARYB_IN_G(
x1)
U3_G(
x1,
x2) =
U3_G(
x1,
x2)
U4_G(
x1,
x2) =
U4_G(
x1,
x2)
U35_AAG(
x1,
x2) =
U35_AAG(
x1,
x2)
U36_AAG(
x1,
x2) =
U36_AAG(
x1,
x2)
U37_AAG(
x1,
x2,
x3,
x4) =
U37_AAG(
x3,
x4)
ADDZJ_IN_AAG(
x1,
x2,
x3) =
ADDZJ_IN_AAG(
x3)
U30_AAG(
x1,
x2,
x3,
x4) =
U30_AAG(
x3,
x4)
ADDZC_IN_AAG(
x1,
x2,
x3) =
ADDZC_IN_AAG(
x3)
U5_AAG(
x1,
x2,
x3,
x4) =
U5_AAG(
x3,
x4)
U6_AAG(
x1,
x2,
x3,
x4) =
U6_AAG(
x3,
x4)
ADDXD_IN_AAG(
x1,
x2,
x3) =
ADDXD_IN_AAG(
x3)
U24_AAG(
x1,
x2) =
U24_AAG(
x1,
x2)
U25_AAG(
x1,
x2) =
U25_AAG(
x1,
x2)
U26_AAG(
x1,
x2,
x3,
x4) =
U26_AAG(
x3,
x4)
U7_AAG(
x1,
x2,
x3,
x4) =
U7_AAG(
x3,
x4)
ADDYE_IN_AAG(
x1,
x2,
x3) =
ADDYE_IN_AAG(
x3)
U27_AAG(
x1,
x2) =
U27_AAG(
x1,
x2)
U28_AAG(
x1,
x2) =
U28_AAG(
x1,
x2)
U29_AAG(
x1,
x2,
x3,
x4) =
U29_AAG(
x3,
x4)
U8_AAG(
x1,
x2,
x3,
x4) =
U8_AAG(
x3,
x4)
ADDCF_IN_AAG(
x1,
x2,
x3) =
ADDCF_IN_AAG(
x3)
U21_AAG(
x1,
x2,
x3) =
U21_AAG(
x2,
x3)
SUCCZH_IN_AG(
x1,
x2) =
SUCCZH_IN_AG(
x2)
U11_AG(
x1,
x2) =
U11_AG(
x1,
x2)
U12_AG(
x1,
x2,
x3) =
U12_AG(
x2,
x3)
SUCCG_IN_AG(
x1,
x2) =
SUCCG_IN_AG(
x2)
U9_AG(
x1,
x2) =
U9_AG(
x1,
x2)
U10_AG(
x1,
x2,
x3) =
U10_AG(
x2,
x3)
U22_AAG(
x1,
x2,
x3) =
U22_AAG(
x2,
x3)
U23_AAG(
x1,
x2,
x3,
x4) =
U23_AAG(
x3,
x4)
ADDCI_IN_AAG(
x1,
x2,
x3) =
ADDCI_IN_AAG(
x3)
U13_AAG(
x1,
x2,
x3,
x4) =
U13_AAG(
x3,
x4)
U14_AAG(
x1,
x2) =
U14_AAG(
x1,
x2)
U15_AAG(
x1,
x2,
x3) =
U15_AAG(
x2,
x3)
U16_AAG(
x1,
x2,
x3,
x4) =
U16_AAG(
x3,
x4)
U17_AAG(
x1,
x2) =
U17_AAG(
x1,
x2)
U18_AAG(
x1,
x2,
x3) =
U18_AAG(
x2,
x3)
U19_AAG(
x1,
x2,
x3,
x4) =
U19_AAG(
x3,
x4)
U20_AAG(
x1,
x2,
x3,
x4) =
U20_AAG(
x3,
x4)
U31_AAG(
x1,
x2,
x3,
x4) =
U31_AAG(
x3,
x4)
U32_AAG(
x1,
x2,
x3,
x4) =
U32_AAG(
x3,
x4)
U33_AAG(
x1,
x2,
x3,
x4) =
U33_AAG(
x3,
x4)
U38_AAG(
x1,
x2) =
U38_AAG(
x1,
x2)
U39_AAG(
x1,
x2) =
U39_AAG(
x1,
x2)
U40_AAG(
x1,
x2,
x3,
x4) =
U40_AAG(
x3,
x4)
U41_AAG(
x1,
x2,
x3,
x4) =
U41_AAG(
x3,
x4)
U42_AAG(
x1,
x2,
x3,
x4) =
U42_AAG(
x3,
x4)
U43_AAG(
x1,
x2,
x3,
x4) =
U43_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
ADDK_IN_AAG(zero(X1), b, zero(X1)) → U34_AAG(X1, binaryZA_in_g(X1))
ADDK_IN_AAG(zero(X1), b, zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(zero(X1)) → U1_G(X1, binaryZA_in_g(X1))
BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(one(X1)) → U2_G(X1, binaryB_in_g(X1))
BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
BINARYB_IN_G(zero(X1)) → U3_G(X1, binaryZA_in_g(X1))
BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYB_IN_G(one(X1)) → U4_G(X1, binaryB_in_g(X1))
BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
ADDK_IN_AAG(one(X1), b, one(X1)) → U35_AAG(X1, binaryB_in_g(X1))
ADDK_IN_AAG(one(X1), b, one(X1)) → BINARYB_IN_G(X1)
ADDK_IN_AAG(b, X1, X1) → U36_AAG(X1, binaryZA_in_g(X1))
ADDK_IN_AAG(b, X1, X1) → BINARYZA_IN_G(X1)
ADDK_IN_AAG(X1, X2, X3) → U37_AAG(X1, X2, X3, addzJ_in_aag(X1, X2, X3))
ADDK_IN_AAG(X1, X2, X3) → ADDZJ_IN_AAG(X1, X2, X3)
ADDZJ_IN_AAG(zero(X1), zero(X2), zero(X3)) → U30_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDZJ_IN_AAG(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(zero(X1), zero(X2), zero(X3)) → U5_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDZC_IN_AAG(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(zero(X1), one(X2), one(X3)) → U6_AAG(X1, X2, X3, addxD_in_aag(X1, X2, X3))
ADDZC_IN_AAG(zero(X1), one(X2), one(X3)) → ADDXD_IN_AAG(X1, X2, X3)
ADDXD_IN_AAG(one(X1), b, one(X1)) → U24_AAG(X1, binaryB_in_g(X1))
ADDXD_IN_AAG(one(X1), b, one(X1)) → BINARYB_IN_G(X1)
ADDXD_IN_AAG(zero(X1), b, zero(X1)) → U25_AAG(X1, binaryZA_in_g(X1))
ADDXD_IN_AAG(zero(X1), b, zero(X1)) → BINARYZA_IN_G(X1)
ADDXD_IN_AAG(X1, X2, X3) → U26_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDXD_IN_AAG(X1, X2, X3) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(one(X1), zero(X2), one(X3)) → U7_AAG(X1, X2, X3, addyE_in_aag(X1, X2, X3))
ADDZC_IN_AAG(one(X1), zero(X2), one(X3)) → ADDYE_IN_AAG(X1, X2, X3)
ADDYE_IN_AAG(b, one(X1), one(X1)) → U27_AAG(X1, binaryB_in_g(X1))
ADDYE_IN_AAG(b, one(X1), one(X1)) → BINARYB_IN_G(X1)
ADDYE_IN_AAG(b, zero(X1), zero(X1)) → U28_AAG(X1, binaryZA_in_g(X1))
ADDYE_IN_AAG(b, zero(X1), zero(X1)) → BINARYZA_IN_G(X1)
ADDYE_IN_AAG(X1, X2, X3) → U29_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDYE_IN_AAG(X1, X2, X3) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(one(X1), one(X2), zero(X3)) → U8_AAG(X1, X2, X3, addcF_in_aag(X1, X2, X3))
ADDZC_IN_AAG(one(X1), one(X2), zero(X3)) → ADDCF_IN_AAG(X1, X2, X3)
ADDCF_IN_AAG(X1, b, X2) → U21_AAG(X1, X2, succZH_in_ag(X1, X2))
ADDCF_IN_AAG(X1, b, X2) → SUCCZH_IN_AG(X1, X2)
SUCCZH_IN_AG(zero(X1), one(X1)) → U11_AG(X1, binaryZA_in_g(X1))
SUCCZH_IN_AG(zero(X1), one(X1)) → BINARYZA_IN_G(X1)
SUCCZH_IN_AG(one(X1), zero(X2)) → U12_AG(X1, X2, succG_in_ag(X1, X2))
SUCCZH_IN_AG(one(X1), zero(X2)) → SUCCG_IN_AG(X1, X2)
SUCCG_IN_AG(zero(X1), one(X1)) → U9_AG(X1, binaryZA_in_g(X1))
SUCCG_IN_AG(zero(X1), one(X1)) → BINARYZA_IN_G(X1)
SUCCG_IN_AG(one(X1), zero(X2)) → U10_AG(X1, X2, succG_in_ag(X1, X2))
SUCCG_IN_AG(one(X1), zero(X2)) → SUCCG_IN_AG(X1, X2)
ADDCF_IN_AAG(b, X1, X2) → U22_AAG(X1, X2, succZH_in_ag(X1, X2))
ADDCF_IN_AAG(b, X1, X2) → SUCCZH_IN_AG(X1, X2)
ADDCF_IN_AAG(X1, X2, X3) → U23_AAG(X1, X2, X3, addCI_in_aag(X1, X2, X3))
ADDCF_IN_AAG(X1, X2, X3) → ADDCI_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(zero(X1), zero(X2), one(X3)) → U13_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDCI_IN_AAG(zero(X1), zero(X2), one(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(zero(zero(X1)), one(b), zero(one(X1))) → U14_AAG(X1, binaryZA_in_g(X1))
ADDCI_IN_AAG(zero(zero(X1)), one(b), zero(one(X1))) → BINARYZA_IN_G(X1)
ADDCI_IN_AAG(zero(one(X1)), one(b), zero(zero(X2))) → U15_AAG(X1, X2, succG_in_ag(X1, X2))
ADDCI_IN_AAG(zero(one(X1)), one(b), zero(zero(X2))) → SUCCG_IN_AG(X1, X2)
ADDCI_IN_AAG(zero(X1), one(X2), zero(X3)) → U16_AAG(X1, X2, X3, addCI_in_aag(X1, X2, X3))
ADDCI_IN_AAG(zero(X1), one(X2), zero(X3)) → ADDCI_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(one(b), zero(zero(X1)), zero(one(X1))) → U17_AAG(X1, binaryZA_in_g(X1))
ADDCI_IN_AAG(one(b), zero(zero(X1)), zero(one(X1))) → BINARYZA_IN_G(X1)
ADDCI_IN_AAG(one(b), zero(one(X1)), zero(zero(X2))) → U18_AAG(X1, X2, succG_in_ag(X1, X2))
ADDCI_IN_AAG(one(b), zero(one(X1)), zero(zero(X2))) → SUCCG_IN_AG(X1, X2)
ADDCI_IN_AAG(one(X1), zero(X2), zero(X3)) → U19_AAG(X1, X2, X3, addCI_in_aag(X1, X2, X3))
ADDCI_IN_AAG(one(X1), zero(X2), zero(X3)) → ADDCI_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(one(X1), one(X2), one(X3)) → U20_AAG(X1, X2, X3, addcF_in_aag(X1, X2, X3))
ADDCI_IN_AAG(one(X1), one(X2), one(X3)) → ADDCF_IN_AAG(X1, X2, X3)
ADDZJ_IN_AAG(zero(X1), one(X2), one(X3)) → U31_AAG(X1, X2, X3, addxD_in_aag(X1, X2, X3))
ADDZJ_IN_AAG(zero(X1), one(X2), one(X3)) → ADDXD_IN_AAG(X1, X2, X3)
ADDZJ_IN_AAG(one(X1), zero(X2), one(X3)) → U32_AAG(X1, X2, X3, addyE_in_aag(X1, X2, X3))
ADDZJ_IN_AAG(one(X1), zero(X2), one(X3)) → ADDYE_IN_AAG(X1, X2, X3)
ADDZJ_IN_AAG(one(X1), one(X2), zero(X3)) → U33_AAG(X1, X2, X3, addcF_in_aag(X1, X2, X3))
ADDZJ_IN_AAG(one(X1), one(X2), zero(X3)) → ADDCF_IN_AAG(X1, X2, X3)
ADDK_IN_AAG(b, zero(X1), zero(X1)) → U38_AAG(X1, binaryZA_in_g(X1))
ADDK_IN_AAG(b, zero(X1), zero(X1)) → BINARYZA_IN_G(X1)
ADDK_IN_AAG(b, one(X1), one(X1)) → U39_AAG(X1, binaryB_in_g(X1))
ADDK_IN_AAG(b, one(X1), one(X1)) → BINARYB_IN_G(X1)
ADDK_IN_AAG(zero(X1), zero(X2), zero(X3)) → U40_AAG(X1, X2, X3, addzC_in_aag(X1, X2, X3))
ADDK_IN_AAG(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDK_IN_AAG(zero(X1), one(X2), one(X3)) → U41_AAG(X1, X2, X3, addxD_in_aag(X1, X2, X3))
ADDK_IN_AAG(zero(X1), one(X2), one(X3)) → ADDXD_IN_AAG(X1, X2, X3)
ADDK_IN_AAG(one(X1), zero(X2), one(X3)) → U42_AAG(X1, X2, X3, addyE_in_aag(X1, X2, X3))
ADDK_IN_AAG(one(X1), zero(X2), one(X3)) → ADDYE_IN_AAG(X1, X2, X3)
ADDK_IN_AAG(one(X1), one(X2), zero(X3)) → U43_AAG(X1, X2, X3, addcF_in_aag(X1, X2, X3))
ADDK_IN_AAG(one(X1), one(X2), zero(X3)) → ADDCF_IN_AAG(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
zero(
x1) =
zero(
x1)
binaryZA_in_g(
x1) =
binaryZA_in_g(
x1)
one(
x1) =
one(
x1)
binaryB_in_g(
x1) =
binaryB_in_g(
x1)
addzJ_in_aag(
x1,
x2,
x3) =
addzJ_in_aag(
x3)
addzC_in_aag(
x1,
x2,
x3) =
addzC_in_aag(
x3)
addxD_in_aag(
x1,
x2,
x3) =
addxD_in_aag(
x3)
addyE_in_aag(
x1,
x2,
x3) =
addyE_in_aag(
x3)
addcF_in_aag(
x1,
x2,
x3) =
addcF_in_aag(
x3)
succZH_in_ag(
x1,
x2) =
succZH_in_ag(
x2)
succG_in_ag(
x1,
x2) =
succG_in_ag(
x2)
addCI_in_aag(
x1,
x2,
x3) =
addCI_in_aag(
x3)
b =
b
ADDK_IN_AAG(
x1,
x2,
x3) =
ADDK_IN_AAG(
x3)
U34_AAG(
x1,
x2) =
U34_AAG(
x1,
x2)
BINARYZA_IN_G(
x1) =
BINARYZA_IN_G(
x1)
U1_G(
x1,
x2) =
U1_G(
x1,
x2)
U2_G(
x1,
x2) =
U2_G(
x1,
x2)
BINARYB_IN_G(
x1) =
BINARYB_IN_G(
x1)
U3_G(
x1,
x2) =
U3_G(
x1,
x2)
U4_G(
x1,
x2) =
U4_G(
x1,
x2)
U35_AAG(
x1,
x2) =
U35_AAG(
x1,
x2)
U36_AAG(
x1,
x2) =
U36_AAG(
x1,
x2)
U37_AAG(
x1,
x2,
x3,
x4) =
U37_AAG(
x3,
x4)
ADDZJ_IN_AAG(
x1,
x2,
x3) =
ADDZJ_IN_AAG(
x3)
U30_AAG(
x1,
x2,
x3,
x4) =
U30_AAG(
x3,
x4)
ADDZC_IN_AAG(
x1,
x2,
x3) =
ADDZC_IN_AAG(
x3)
U5_AAG(
x1,
x2,
x3,
x4) =
U5_AAG(
x3,
x4)
U6_AAG(
x1,
x2,
x3,
x4) =
U6_AAG(
x3,
x4)
ADDXD_IN_AAG(
x1,
x2,
x3) =
ADDXD_IN_AAG(
x3)
U24_AAG(
x1,
x2) =
U24_AAG(
x1,
x2)
U25_AAG(
x1,
x2) =
U25_AAG(
x1,
x2)
U26_AAG(
x1,
x2,
x3,
x4) =
U26_AAG(
x3,
x4)
U7_AAG(
x1,
x2,
x3,
x4) =
U7_AAG(
x3,
x4)
ADDYE_IN_AAG(
x1,
x2,
x3) =
ADDYE_IN_AAG(
x3)
U27_AAG(
x1,
x2) =
U27_AAG(
x1,
x2)
U28_AAG(
x1,
x2) =
U28_AAG(
x1,
x2)
U29_AAG(
x1,
x2,
x3,
x4) =
U29_AAG(
x3,
x4)
U8_AAG(
x1,
x2,
x3,
x4) =
U8_AAG(
x3,
x4)
ADDCF_IN_AAG(
x1,
x2,
x3) =
ADDCF_IN_AAG(
x3)
U21_AAG(
x1,
x2,
x3) =
U21_AAG(
x2,
x3)
SUCCZH_IN_AG(
x1,
x2) =
SUCCZH_IN_AG(
x2)
U11_AG(
x1,
x2) =
U11_AG(
x1,
x2)
U12_AG(
x1,
x2,
x3) =
U12_AG(
x2,
x3)
SUCCG_IN_AG(
x1,
x2) =
SUCCG_IN_AG(
x2)
U9_AG(
x1,
x2) =
U9_AG(
x1,
x2)
U10_AG(
x1,
x2,
x3) =
U10_AG(
x2,
x3)
U22_AAG(
x1,
x2,
x3) =
U22_AAG(
x2,
x3)
U23_AAG(
x1,
x2,
x3,
x4) =
U23_AAG(
x3,
x4)
ADDCI_IN_AAG(
x1,
x2,
x3) =
ADDCI_IN_AAG(
x3)
U13_AAG(
x1,
x2,
x3,
x4) =
U13_AAG(
x3,
x4)
U14_AAG(
x1,
x2) =
U14_AAG(
x1,
x2)
U15_AAG(
x1,
x2,
x3) =
U15_AAG(
x2,
x3)
U16_AAG(
x1,
x2,
x3,
x4) =
U16_AAG(
x3,
x4)
U17_AAG(
x1,
x2) =
U17_AAG(
x1,
x2)
U18_AAG(
x1,
x2,
x3) =
U18_AAG(
x2,
x3)
U19_AAG(
x1,
x2,
x3,
x4) =
U19_AAG(
x3,
x4)
U20_AAG(
x1,
x2,
x3,
x4) =
U20_AAG(
x3,
x4)
U31_AAG(
x1,
x2,
x3,
x4) =
U31_AAG(
x3,
x4)
U32_AAG(
x1,
x2,
x3,
x4) =
U32_AAG(
x3,
x4)
U33_AAG(
x1,
x2,
x3,
x4) =
U33_AAG(
x3,
x4)
U38_AAG(
x1,
x2) =
U38_AAG(
x1,
x2)
U39_AAG(
x1,
x2) =
U39_AAG(
x1,
x2)
U40_AAG(
x1,
x2,
x3,
x4) =
U40_AAG(
x3,
x4)
U41_AAG(
x1,
x2,
x3,
x4) =
U41_AAG(
x3,
x4)
U42_AAG(
x1,
x2,
x3,
x4) =
U42_AAG(
x3,
x4)
U43_AAG(
x1,
x2,
x3,
x4) =
U43_AAG(
x3,
x4)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 70 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- BINARYB_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
The graph contains the following edges 1 > 1
- BINARYB_IN_G(one(X1)) → BINARYB_IN_G(X1)
The graph contains the following edges 1 > 1
- BINARYZA_IN_G(zero(X1)) → BINARYZA_IN_G(X1)
The graph contains the following edges 1 > 1
- BINARYZA_IN_G(one(X1)) → BINARYB_IN_G(X1)
The graph contains the following edges 1 > 1
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUCCG_IN_AG(one(X1), zero(X2)) → SUCCG_IN_AG(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
zero(
x1) =
zero(
x1)
one(
x1) =
one(
x1)
SUCCG_IN_AG(
x1,
x2) =
SUCCG_IN_AG(
x2)
We have to consider all (P,R,Pi)-chains
(15) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUCCG_IN_AG(zero(X2)) → SUCCG_IN_AG(X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(17) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- SUCCG_IN_AG(zero(X2)) → SUCCG_IN_AG(X2)
The graph contains the following edges 1 > 1
(18) YES
(19) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
ADDXD_IN_AAG(X1, X2, X3) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(zero(X1), zero(X2), zero(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(zero(X1), one(X2), one(X3)) → ADDXD_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(one(X1), zero(X2), one(X3)) → ADDYE_IN_AAG(X1, X2, X3)
ADDYE_IN_AAG(X1, X2, X3) → ADDZC_IN_AAG(X1, X2, X3)
ADDZC_IN_AAG(one(X1), one(X2), zero(X3)) → ADDCF_IN_AAG(X1, X2, X3)
ADDCF_IN_AAG(X1, X2, X3) → ADDCI_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(zero(X1), zero(X2), one(X3)) → ADDZC_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(zero(X1), one(X2), zero(X3)) → ADDCI_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(one(X1), zero(X2), zero(X3)) → ADDCI_IN_AAG(X1, X2, X3)
ADDCI_IN_AAG(one(X1), one(X2), one(X3)) → ADDCF_IN_AAG(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
zero(
x1) =
zero(
x1)
one(
x1) =
one(
x1)
ADDZC_IN_AAG(
x1,
x2,
x3) =
ADDZC_IN_AAG(
x3)
ADDXD_IN_AAG(
x1,
x2,
x3) =
ADDXD_IN_AAG(
x3)
ADDYE_IN_AAG(
x1,
x2,
x3) =
ADDYE_IN_AAG(
x3)
ADDCF_IN_AAG(
x1,
x2,
x3) =
ADDCF_IN_AAG(
x3)
ADDCI_IN_AAG(
x1,
x2,
x3) =
ADDCI_IN_AAG(
x3)
We have to consider all (P,R,Pi)-chains
(20) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ADDXD_IN_AAG(X3) → ADDZC_IN_AAG(X3)
ADDZC_IN_AAG(zero(X3)) → ADDZC_IN_AAG(X3)
ADDZC_IN_AAG(one(X3)) → ADDXD_IN_AAG(X3)
ADDZC_IN_AAG(one(X3)) → ADDYE_IN_AAG(X3)
ADDYE_IN_AAG(X3) → ADDZC_IN_AAG(X3)
ADDZC_IN_AAG(zero(X3)) → ADDCF_IN_AAG(X3)
ADDCF_IN_AAG(X3) → ADDCI_IN_AAG(X3)
ADDCI_IN_AAG(one(X3)) → ADDZC_IN_AAG(X3)
ADDCI_IN_AAG(zero(X3)) → ADDCI_IN_AAG(X3)
ADDCI_IN_AAG(one(X3)) → ADDCF_IN_AAG(X3)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(22) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- ADDZC_IN_AAG(one(X3)) → ADDXD_IN_AAG(X3)
The graph contains the following edges 1 > 1
- ADDZC_IN_AAG(zero(X3)) → ADDZC_IN_AAG(X3)
The graph contains the following edges 1 > 1
- ADDXD_IN_AAG(X3) → ADDZC_IN_AAG(X3)
The graph contains the following edges 1 >= 1
- ADDYE_IN_AAG(X3) → ADDZC_IN_AAG(X3)
The graph contains the following edges 1 >= 1
- ADDCI_IN_AAG(one(X3)) → ADDZC_IN_AAG(X3)
The graph contains the following edges 1 > 1
- ADDZC_IN_AAG(one(X3)) → ADDYE_IN_AAG(X3)
The graph contains the following edges 1 > 1
- ADDZC_IN_AAG(zero(X3)) → ADDCF_IN_AAG(X3)
The graph contains the following edges 1 > 1
- ADDCF_IN_AAG(X3) → ADDCI_IN_AAG(X3)
The graph contains the following edges 1 >= 1
- ADDCI_IN_AAG(one(X3)) → ADDCF_IN_AAG(X3)
The graph contains the following edges 1 > 1
- ADDCI_IN_AAG(zero(X3)) → ADDCI_IN_AAG(X3)
The graph contains the following edges 1 > 1
(23) YES